Section: New Software and Platforms

Cubicle

The Cubicle model checker modulo theories

Keywords: Model Checking - Software Verification

Functional Description

Cubicle is an open source model checker for verifying safety properties of array-based systems, which corresponds to a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems.

• Participants: Sylvain Conchon and Alain Mebsout

• Contact: Sylvain Conchon

• URL: http://cubicle.lri.fr/